Buffer overflows are a common cause of security vulnerabilities in systems code. Specifically, buffer overflow occurs when a process stores data in a buffer outside of the memory allocated for the process. The overflow can cause diverse errors including erratic program behavior, memory access errors, incorrect results, program crashes, and security breaches. A variety of techniques have been used to attempt to locate buffer overflows in code before they occur, including both dynamic and static techniques. One such technique is symbolic analysis.
Symbolic analysis was originally introduced more than 30 years ago, and has been applied in a variety of manners such as parallelization, optimization, and bug detection. The symbolic expressions resulting from symbolic analysis are typically so large and complex that external mathematical libraries are needed to solve them. As expected, these complex expressions cause symbolic analysis to be of limited use when dealing with large amounts of variables and/or large amounts of code, due to the time required to process the code. While various techniques have been developed to speed up the symbolic analysis processes, the efficiencies gained from the various techniques typically come at the cost of less accurate results.